VERS5 
NIL 
((DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (DISJUNCTIVE_SYLLOGISM NORMAL#9) (IRREFLEXIVITY_OF_ORDER NATNUM#7) (TRANSITIVITY_OF_ORDER NATNUM#8) (ZEROLEAST1 NATNUM#9) (SUCCESSOR1 NATNUM#11) (SUCCESSOR2 NATNUM#12) (SUCCESSORLESS NATNUM#13) (SUCCESSOREQ NATNUM#14) (ZEROLEAST2 NATNUM#15) (ZEROLEAST3 NATNUM#16) (ZERO_NOT_SUCCESSOR NATNUM#17) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (COMMUTADD NATNUM#29) (TIMSUCC NATNUM#33) (LTIMESCAN NATNUM#34) (RTIMESCAN NATNUM#35) (COMMUTMULT NATNUM#36) (LTIMESTOZERO NATNUM#37) (RTIMESTOZERO NATNUM#38) (LDISTRIB NATNUM#39) (RDISTRIB NATNUM#40) (PROOF_BY_INDUCTION INDUCTION#1) (INDUCTIVE_DEFINITION INDUCTION#5) (PROOF_BY_DOUBLEINDUCTION INDUCTION#6) (HIGH_ORDER_NATNUM_DEFINITION INDUCTION#10) (INFINITE_DESCENT INDUCTION#11) (LESSEQDEF LESSEQ#2) (SUCCESSORLESSEQ LESSEQ#3) (SUCCESSORFACTS LESSEQ#3) (TRANS_LESSEQ LESSEQ#4) (LESS_LESSEQ_FACT1 LESSEQ#5) (ZEROLEAST LESSEQ#6) (ONELEASTSUCC LESSEQ#7) (ZERO_NON_LESS_SUCCESSOR LESSEQ#8) (SUCC_LESS_LESS LESSEQ#9) (SUCC_LESSEQ_LESSEQ LESSEQ#10) (LESSEQ_LESSEQ_SUCC LESSEQ#11) (LESS_SUCC_LESSEQ LESSEQ#12) (LESS_LESSEQSUCC LESSEQ#13) (LEQ_LEQ_EQ LESSEQ#15) (TRICHOTOMY LESSEQ#16) (MINUSDEF MINUS#2) (MINUS_SORT MINUS#3) (MINUSFACT3 MINUS#4) (MINUSFACT5 MINUS#5) (SUCCESSOR_MINUS MINUS#6) (MINUSFACT10 MINUS#7) (MINUSFACT11 MINUS#8) (N_LESS_N MINUS#9) (MINUS1 MINUS#10) (TOTAL_SUBTRACTION MINUS#11) (INEQUALITY_LAW MINUS#12) (ADD_LESSEQ MINUS#13) (ADD_ONE MINUS#14) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (SUCCFACTS NATNUM#11 NATNUM#12 NATNUM#13 NATNUM#14 NATNUM#15 NATNUM#16 NATNUM#17) (TIMESFACTS NATNUM#30 NATNUM#32 NATNUM#33 NATNUM#34 NATNUM#35 NATNUM#36 NATNUM#37 NATNUM#38 NATNUM#39 NATNUM#40) (PLUSFACTS NATNUM#21 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 NATNUM#29 NATNUM#39 NATNUM#40) (SIMPINFO NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#3 LESSEQ#8 LESSEQ#14 MINUS#3 MINUS#9)) (|∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R|)) . ((R . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (Q . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . NATNUM#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 5 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 6 .)(NIL . (DECL LESSEQ (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . LESSEQ . NIL . 1 .)(NIL . (DECL MINUS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (INFIXNAME: -) (BINDINGPOWER: 940)) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . MINUS . NIL . 1 .)(|∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q|)) . (R Q P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R|)) . (R Q P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)| . (AXIOM (TM& . |∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)|)) . (R Q P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P Q.¬(P∨Q)≡¬P∧¬Q| . (AXIOM (TM& . |∀P Q.¬(P∨Q)≡¬P∧¬Q|)) . (R Q P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P Q.¬(P∧Q)≡¬P∨¬Q| . (AXIOM (TM& . |∀P Q.¬(P∧Q)≡¬P∨¬Q|)) . (R Q P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P Q.P≡(Q⊃P)∧(¬Q⊃P)| . (AXIOM (TM& . |∀P Q.P≡(Q⊃P)∧(¬Q⊃P)|)) . (R Q P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R| . (DERIVE (TM& . |∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R|) ((LR&)) NIL) . (R Q P) . NIL . NIL . NIL . NORMAL . NIL . 8 .)(|∀PSI THETA.(∀XW.PSI(XW)⊃THETA(XW))∧(∀XW.¬PSI(XW)⊃THETA(XW))⊃(∀XW.THETA(XW))| . (AXIOM (TM& . |∀PSI THETA.(∀XW.PSI(XW)⊃THETA(XW))∧(∀XW.¬PSI(XW)⊃THETA(XW))⊃(∀XW.THETA(XW))|)) . ((XW . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .)) (THETA . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .)) (PSI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .))) . NIL . (NORMAL#9) . NIL . NORMAL . NIL . 9 .)(|∀N.¬N<N| . (AXIOM (TM& . |∀N.¬N<N|)) . (LESSP M N K J I) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (LESSP M N K J I) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (LESSP M N K J I) . NIL . (NATNUM#9) . NIL . NATNUM . NIL . 9 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (ADD1 M N K J I) . NIL . (NATNUM#10) . NIL . NATNUM . NIL . 10 .)(|∀N.N<N'| . (AXIOM (TM& . |∀N.N<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#11) . NIL . NATNUM . NIL . 11 .)(|∀N M.¬N<M⊃M<N'| . (AXIOM (TM& . |∀N M.¬N<M⊃M<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#12) . NIL . NATNUM . NIL . 12 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (ADD1 M N K J I) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (LESSP M N K J I) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.0<N'| . (AXIOM (TM& . |∀N.0<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (ADD1 M N K J I) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(NIL . (DECL PRED (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#18 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 18 .)(|∀N.PRED(N')=N| . (DEFAX PRED (TM& . |∀N.PRED(N')=N|)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#19 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (ADD1 M N K J I SET C B A) . NIL . (INDUCTION#1) . NIL . INDUCTION . NIL . 1 .)(NIL . (DECL NPARS (TYPE: (TY& . GROUND*))) . ((NPARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 2 .)(NIL . (DECL NDF (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((NDF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 3 .)(NIL . (DECL ZCASE (TYPE: (TY& . |(GROUND*)→GROUND|))) . ((ZCASE . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 4 .)(|∀N.NATNUM(PRED(N))| . (AXIOM (TM& . |∀N.NATNUM(PRED(N))|)) . (ADD1 M N K J I PRED) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#21 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))| . (AXIOM (TM& . |∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))|)) . (ADD1 M N K J I NPARS NDF ZCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .)) (NDEF . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .))) . NIL . (INDUCTION#5) . NIL . INDUCTION . NIL . 5 .)(|∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))| . (AXIOM (TM& . |∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))|)) . (ADD1 M N K J I (A2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#6 . NIL . VARIABLE .))) . NIL . (INDUCTION#6) . NIL . INDUCTION . NIL . 6 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 7 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#29) . NIL . NATNUM . NIL . 29 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#30 . NIL . DEFINED .)) ADD1 PLUS M N K J I) . NIL . (NATNUM#30) . NIL . NATNUM . NIL . 30 .)(NIL . (DECL INDFN (TYPE: (TY& . |(GROUND⊗(@ARB))→(@ARB)|))) . ((INDFN . (|(GROUND⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#8 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 8 .)(NIL . (DECL (DEF_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((DEF_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#9 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 9 .)(|∀N M.NATNUM(M*N)| . (AXIOM (TM& . |∀N M.NATNUM(M*N)|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#31) . NIL . NATNUM . NIL . 31 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#32) . NIL . NATNUM . NIL . 32 .)(|∀N K.N*K'=N*K+N| . (AXIOM (TM& . |∀N K.N*K'=N*K+N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#33) . NIL . NATNUM . NIL . 33 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#34) . NIL . NATNUM . NIL . 34 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#35) . NIL . NATNUM . NIL . 35 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#36) . NIL . NATNUM . NIL . 36 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#37) . NIL . NATNUM . NIL . 37 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#38) . NIL . NATNUM . NIL . 38 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#39) . NIL . NATNUM . NIL . 39 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#40) . NIL . NATNUM . NIL . 40 .)(|∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))| . (AXIOM (TM& . |∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))|)) . (ADD1 M N K J I ARB2 ARB1 ARB INDFN DEF_FUN) . NIL . (INDUCTION#10) . NIL . INDUCTION . NIL . 10 .)(|¬(∃DESC.(∀N.DESC(N')<DESC(N)))| . (AXIOM (TM& . |¬(∃DESC.(∀N.DESC(N')<DESC(N)))|)) . (LESSP ADD1 M N K J I (DESC . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#11 . NIL . VARIABLE .))) . NIL . (INDUCTION#11) . NIL . INDUCTION . NIL . 11 .)(|∀M N.M≤N=(M=N∨M<N)| . (DEFINE LESSEQ (TM& . |∀M N.M≤N=(M=N∨M<N)|) NIL) . (LESSP M N K J I (LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#2 . NIL . DEFINED .))) . NIL . (LESSEQ#2 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16) . NIL . LESSEQ . NIL . 2 .)(|∀N M.N'≤M'≡N≤M| . (AXIOM (TM& . |∀N M.N'≤M'≡N≤M|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#3) . NIL . LESSEQ . NIL . 3 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#4) . NIL . LESSEQ . NIL . 4 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#5) . NIL . LESSEQ . NIL . 5 .)(|∀N.0≤N| . (AXIOM (TM& . |∀N.0≤N|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#6) . NIL . LESSEQ . NIL . 6 .)(|∀N.1≤N'| . (AXIOM (TM& . |∀N.1≤N'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#7) . NIL . LESSEQ . NIL . 7 .)(|∀N M.N'<M⊃¬M=0| . (AXIOM (TM& . |∀N M.N'<M⊃¬M=0|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#8) . NIL . LESSEQ . NIL . 8 .)(|∀M N.M'<N⊃M<N| . (AXIOM (TM& . |∀M N.M'<N⊃M<N|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#9) . NIL . LESSEQ . NIL . 9 .)(|∀M N.M'≤N⊃M≤N| . (AXIOM (TM& . |∀M N.M'≤N⊃M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#10) . NIL . LESSEQ . NIL . 10 .)(|∀N M.N≤M⊃N≤M'| . (AXIOM (TM& . |∀N M.N≤M⊃N≤M'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#11) . NIL . LESSEQ . NIL . 11 .)(|∀N M.M<N'≡M≤N| . (AXIOM (TM& . |∀N M.M<N'≡M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#12) . NIL . LESSEQ . NIL . 12 .)(|∀M N.M<N=M'≤N| . (AXIOM (TM& . |∀M N.M<N=M'≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#13) . NIL . LESSEQ . NIL . 13 .)(|∀N.¬N=N'| . (AXIOM (TM& . |∀N.¬N=N'|)) . (ADD1 M N K J I) . NIL . (LESSEQ#14) . NIL . LESSEQ . NIL . 14 .)(|∀N M.N≤M∧M≤N⊃N=M| . (AXIOM (TM& . |∀N M.N≤M∧M≤N⊃N=M|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#15) . NIL . LESSEQ . NIL . 15 .)(|∀N M.M<N∨M=N∨N<M| . (AXIOM (TM& . |∀N M.M<N∨M=N∨N<M|)) . (LESSP M N K J I) . NIL . (LESSEQ#16) . NIL . LESSEQ . NIL . 16 .)(|∀M N.M-0=M∧M-N'=PRED(M-N)| . (DEFINE MINUS (TM& . |∀M N.M-0=M∧M-N'=PRED(M-N)|) (USE (LR& INDUCTION#5))) . (ADD1 M N K J I PRED (MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#2 . NIL . DEFINED .))) . NIL . (MINUS#2 INDUCTION#5 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#3 LESSEQ#8 LESSEQ#14) . NIL . MINUS . NIL . 2 .)(|∀N K.NATNUM(K-N)| . (AXIOM (TM& . |∀N K.NATNUM(K-N)|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#3) . NIL . MINUS . NIL . 3 .)(|∀N M.N<M⊃0<M-N| . (AXIOM (TM& . |∀N M.N<M⊃0<M-N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#4) . NIL . MINUS . NIL . 4 .)(|∀N.0<N⊃PRED(N)'=N| . (AXIOM (TM& . |∀N.0<N⊃PRED(N)'=N|)) . (LESSP ADD1 M N K J I PRED) . NIL . (MINUS#5) . NIL . MINUS . NIL . 5 .)(|∀N M.N≤M⊃M'-N=(M-N)'| . (AXIOM (TM& . |∀N M.N≤M⊃M'-N=(M-N)'|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#6) . NIL . MINUS . NIL . 6 .)(|∀N M.N<M⊃M-N=(M-N')'| . (AXIOM (TM& . |∀N M.N<M⊃M-N=(M-N')'|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#7) . NIL . MINUS . NIL . 7 .)(|∀N M.M<N⊃N-M'<N| . (AXIOM (TM& . |∀N M.M<N⊃N-M'<N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#8) . NIL . MINUS . NIL . 8 .)(|∀N.N-N=0| . (AXIOM (TM& . |∀N.N-N=0|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#9) . NIL . MINUS . NIL . 9 .)(|∀N.0<N⊃N-PRED(N)=1| . (AXIOM (TM& . |∀N.0<N⊃N-PRED(N)=1|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#10) . NIL . MINUS . NIL . 10 .)(|∀N M.M≤N⊃M-N=0| . (AXIOM (TM& . |∀N M.M≤N⊃M-N=0|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#11) . NIL . MINUS . NIL . 11 .)(|∀N M K.K<N∧M<N-K≡M+K<N| . (AXIOM (TM& . |∀N M K.K<N∧M<N-K≡M+K<N|)) . (LESSP ADD1 PLUS M N K J I PRED MINUS) . NIL . (MINUS#12) . NIL . MINUS . NIL . 12 .)(|∀N K M.N≤M∧1≤K⊃N'≤M+K| . (AXIOM (TM& . |∀N K M.N≤M∧1≤K⊃N'≤M+K|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#13) . NIL . MINUS . NIL . 13 .)(|∀K N M.1≤K∧N'=M+K∧N≤M⊃1=K∧N=M| . (AXIOM (TM& . |∀K N M.1≤K∧N'=M+K∧N≤M⊃1=K∧N=M|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#14) . NIL . MINUS . NIL . 14 .)